Search for: All records

Machine learning accelerators (MLAs) are increasingly im- portant in many applications such as image and video processing, speech recognition, and natural language processing. To achieve the needed per- formances and power efficiencies, MLAs are highly concurrent. The cor- rectness of MLAs hinges on the concept of sequential consistency, i.e., the concurrent execution of a program by an MLA must be equivalent to a sequential execution of the program. In this paper, we certify the sequential consistency of modular MLAs using theorem proving. We őrst provide a formalization of the MLAs and deőne their sequential consis- tency. After that, we introduce our certiőcation methodology based on inductive theorem proving. Finally, we demonstrate the feasibility of our approach through the analysis of the NVIDIA Deep Learning Accelerator and the Versatile Tensor Accelerator 

JavaScript has become the most popular programming language for web front-end development. With such popularity, there is a great demand for thorough testing of client-side JavaScript web applications. In this paper, we present a novel approach to concolic testing of front-end JavaScript web applications. This approach leverages widely used JavaScript testing frameworks such as Jest and Puppeteer and conducts concolic execution on JavaScript functions in web applications for unit testing. The seamless integration of concolic testing with these testing frameworks allows injection of symbolic variables within the native execution context of a JavaScript web function and precise capture of concrete execution traces of the function under test. Such concise execution traces greatly improve the effectiveness and efficiency of the subsequent symbolic analysis for test generation. We have implemented our approach on Jest and Puppeteer. The application of our Jest implementation on Metamask, one of the most popular Crypto wallets, has uncovered 3 bugs and 1 test suite improvement, whose bug reports have all been accepted by Metamask developers on Github. We also applied our Puppeteer implementation to 21 Github projects and detected 4 bugs. 

JavaScript (JS) has evolved into a versatile and popular programming language for not only the web, but also a wide range of server-side and client-side applications. Effective, efficient, and easy-to-use testing techniques for JS scripts are in great demand. In this paper, we introduce a holistic approach to applying concolic testing to JS scripts in-situ, i.e., JS scripts are executed in their native environments as part of concolic execution and test cases generated are directly replayed in these environments. We have implemented this approach in the context of Node.js, a JS runtime built on top of Chrome’s V8 JS engine, and evaluated its effectiveness and efficiency through application to 180 Node.js libraries with heavy use of string operations. For 85% of these libraries, it achieved statement coverage ranging between 75% and 100%, a close match in coverage with the hand-crafted unit test suites accompanying their NPM releases. Our approach detected numerous exceptions in these libraries. We analyzed the exception reports for 12 representative libraries and found 6 bugs in these libraries, 4 of which are previously undetected. The bug reports and patches that we filed for these bugs have been accepted by the library developers on GitHub. 

Attackers rely upon a vast array of tools for automating attacksagainst vulnerable servers and services. It is often the case thatwhen vulnerabilities are disclosed, scripts for detecting and exploit-ing them in tools such asNmapandMetasploitare released soonafter, leading to the immediate identification and compromise ofvulnerable systems. Honeypots, honeynets, tarpits, and other decep-tive techniques can be used to slow attackers down, however, such approaches have difficulty keeping up with the sheer number of vulnerabilities being discovered and attacking scripts that are being released. To address this issue, this paper describes an approach for applying concolic execution on attacking scripts in Nmap in order to automatically generate lightweight fake versions of the vulnerable services that can fool the scripts. By doing so in an automated and scalable manner, the approach can enable rapid deployment of custom honeyfarms that leverage the results of concolic execution to trick an attacker's script into returning a result chosen by the honeyfarm, making the script unreliable for the use by the attacker. 

Abstract X-ray polarization is a unique new probe of the particle acceleration in astrophysical jets made possible through the Imaging X-ray Polarimetry Explorer. Here we report on the first dense X-ray polarization monitoring campaign on the blazar Mrk 421. Our observations were accompanied by an even denser radio and optical polarization campaign. We find significant short-timescale variability in both X-ray polarization degree and angle, including an ∼90° angle rotation about the jet axis. We attribute this to random variations of the magnetic field, consistent with the presence of turbulence but also unlikely to be explained by turbulence alone. At the same time, the degree of lower-energy polarization is significantly lower and shows no more than mild variability. Our campaign provides further evidence for a scenario in which energy-stratified shock-acceleration of relativistic electrons, combined with a turbulent magnetic field, is responsible for optical to X-ray synchrotron emission in blazar jets. 

Abstract We report the Imaging X-ray Polarimetry Explorer (IXPE) polarimetric and simultaneous multiwavelength observations of the high-energy-peaked BL Lacertae object (HBL) 1ES 1959+650, performed in 2022 October and 2023 August. In 2022 October, IXPE measured an average polarization degree Π_X= 9.4% ± 1.6% and an electric-vector position angleψ_X= 53° ± 5°. The polarized X-ray emission can be decomposed into a constant component, plus a rotating component, with the rotation velocityω_EVPA= (−117 ± 12) deg day⁻¹. In 2023 August, during a period of pronounced activity of the source, IXPE measured an average Π_X= 12.4% ± 0.7% andψ_X= 20° ± 2°, with evidence (∼0.4% chance probability) for a rapidly rotating component withω_EVPA= 1864 ± 34 deg day⁻¹. These findings suggest the presence of a helical magnetic field in the jet of 1ES 1959+650 or stochastic processes governing the field in turbulent plasma. Our multiwavelength campaigns from radio to X-ray reveal variability in both polarization and flux from optical to X-rays. We interpret the results in terms of a relatively slowly varying component dominating the radio and optical emission, while rapidly variable polarized components dominate the X-ray and provide minor contribution at optical wavelengths. The radio and optical data indicate that on parsec scales the magnetic field is primarily orthogonal to the jet direction. On the contrary, X-ray measurements show a magnetic field almost aligned with the parsec jet direction. Confronting with other IXPE observations, we guess that the magnetic field of HBLs on subparsec scale should be rather unstable, often changing its direction with respect to the Very Long Baseline Array jet. 

Abstract Blazars, supermassive black hole systems with highly relativistic jets aligned with the line of sight, are the most powerful long-lived emitters of electromagnetic emission in the Universe. We report here on a radio-to-gamma-ray multiwavelength campaign on the blazar BL Lacertae with unprecedented polarimetric coverage from radio to X-ray wavelengths. The observations caught an extraordinary event on 2023 November 10–18, when the degree of linear polarization of optical synchrotron radiation reached a record value of 47.5%. In stark contrast, the Imaging X-ray Polarimetry Explorer found that the X-ray (Compton scattering or hadron-induced) emission was polarized at less than 7.4% (3σconfidence level). We argue here that this observational result rules out a hadronic origin of the high-energy emission and strongly favors a leptonic (Compton scattering) origin, thereby breaking the degeneracy between hadronic and leptonic emission models for BL Lacertae and demonstrating the power of multiwavelength polarimetry to address this question. Furthermore, the multiwavelength flux and polarization variability, featuring an extremely prominent rise and decay of the optical polarization degree, is interpreted for the first time by the relaxation of a magnetic “spring” embedded in the newly injected plasma. This suggests that the plasma jet can maintain a predominant toroidal magnetic field component parsecs away from the central engine. 

Paleomagnetic, rock magnetic, or geomagnetic data found in the MagIC data repository from a paper titled: New archaeomagnetic direction results from China and their constraints on palaeosecular variation of the geomagnetic field in Eastern Asia